Termination w.r.t. Q proof of /tmp/tmphmsAI

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z)
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

Q is empty.

↳ QTRS

  ↳ AAECC Innermost

Q restricted rewrite system:
The TRS R consists of the following rules:

f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z)
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

Q is empty.

We have applied [19,8] to switch to innermost. The TRS R 1 is

plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The TRS R 2 is

f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z)
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z))

The signature Sigma is {f}

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z)
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

f(true, x0, x1, x2)
plus(x0, 0)
plus(x0, s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

F(true, x, y, z) → GT(x, plus(y, z))
F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z)
F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z))
GT(s(u), s(v)) → GT(u, v)
PLUS(n, s(m)) → PLUS(n, m)
F(true, x, y, z) → PLUS(y, z)

The TRS R consists of the following rules:

f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z)
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

f(true, x0, x1, x2)
plus(x0, 0)
plus(x0, s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

F(true, x, y, z) → GT(x, plus(y, z))
F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z)
F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z))
GT(s(u), s(v)) → GT(u, v)
PLUS(n, s(m)) → PLUS(n, m)
F(true, x, y, z) → PLUS(y, z)

The TRS R consists of the following rules:

f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z)
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

f(true, x0, x1, x2)
plus(x0, 0)
plus(x0, s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 3 SCCs with 2 less nodes.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GT(s(u), s(v)) → GT(u, v)

The TRS R consists of the following rules:

f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z)
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

f(true, x0, x1, x2)
plus(x0, 0)
plus(x0, s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GT(s(u), s(v)) → GT(u, v)

R is empty.
The set Q consists of the following terms:

f(true, x0, x1, x2)
plus(x0, 0)
plus(x0, s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

f(true, x0, x1, x2)
plus(x0, 0)
plus(x0, s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GT(s(u), s(v)) → GT(u, v)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

GT(s(u), s(v)) → GT(u, v)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PLUS(n, s(m)) → PLUS(n, m)

The TRS R consists of the following rules:

f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z)
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

f(true, x0, x1, x2)
plus(x0, 0)
plus(x0, s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PLUS(n, s(m)) → PLUS(n, m)

R is empty.
The set Q consists of the following terms:

f(true, x0, x1, x2)
plus(x0, 0)
plus(x0, s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

f(true, x0, x1, x2)
plus(x0, 0)
plus(x0, s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PLUS(n, s(m)) → PLUS(n, m)

From the DPs we obtained the following set of size-change graphs:

PLUS(n, s(m)) → PLUS(n, m)
The graph contains the following edges 1 >= 1, 2 > 2

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z)
F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z))

The TRS R consists of the following rules:

f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z)
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

f(true, x0, x1, x2)
plus(x0, 0)
plus(x0, s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z)
F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z))

The TRS R consists of the following rules:

plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

f(true, x0, x1, x2)
plus(x0, 0)
plus(x0, s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

f(true, x0, x1, x2)

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ NonInfProof

Q DP problem:
The TRS P consists of the following rules:

F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z)
F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z))

The TRS R consists of the following rules:

plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

plus(x0, 0)
plus(x0, s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The DP Problem is simplified using the Induction Calculus [18] with the following steps:
Note that final constraints are written in bold face.

For Pair F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z) the following chains were created:

We consider the chain F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z), F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z) which results in the following constraint:
(1)    (F(gt(x0, plus(x1, x2)), x0, s(x1), x2)=F(true, x3, x4, x5) ⇒ F(true, x3, x4, x5)≥F(gt(x3, plus(x4, x5)), x3, s(x4), x5))

We simplified constraint (1) using rules (I), (II), (III), (VII) which results in the following new constraint:
(2)    (plus(x1, x2)=x24∧gt(x0, x24)=true ⇒ F(true, x0, s(x1), x2)≥F(gt(x0, plus(s(x1), x2)), x0, s(s(x1)), x2))

We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on gt(x0, x24)=true which results in the following new constraints:
(3)    (true=true∧plus(x1, x2)=0 ⇒ F(true, s(x26), s(x1), x2)≥F(gt(s(x26), plus(s(x1), x2)), s(x26), s(s(x1)), x2))

(4)    (gt(x27, x28)=true∧plus(x1, x2)=s(x28)∧(∀x29,x30:gt(x27, x28)=true∧plus(x29, x30)=x28 ⇒ F(true, x27, s(x29), x30)≥F(gt(x27, plus(s(x29), x30)), x27, s(s(x29)), x30)) ⇒ F(true, s(x27), s(x1), x2)≥F(gt(s(x27), plus(s(x1), x2)), s(x27), s(s(x1)), x2))

We simplified constraint (3) using rules (I), (II) which results in the following new constraint:
(5)    (plus(x1, x2)=0 ⇒ F(true, s(x26), s(x1), x2)≥F(gt(s(x26), plus(s(x1), x2)), s(x26), s(s(x1)), x2))

We simplified constraint (4) using rule (V) (with possible (I) afterwards) using induction on plus(x1, x2)=s(x28) which results in the following new constraints:
(6)    (x34=s(x28)∧gt(x27, x28)=true∧(∀x29,x30:gt(x27, x28)=true∧plus(x29, x30)=x28 ⇒ F(true, x27, s(x29), x30)≥F(gt(x27, plus(s(x29), x30)), x27, s(s(x29)), x30)) ⇒ F(true, s(x27), s(x34), 0)≥F(gt(s(x27), plus(s(x34), 0)), s(x27), s(s(x34)), 0))

(7)    (s(plus(x35, x36))=s(x28)∧gt(x27, x28)=true∧(∀x29,x30:gt(x27, x28)=true∧plus(x29, x30)=x28 ⇒ F(true, x27, s(x29), x30)≥F(gt(x27, plus(s(x29), x30)), x27, s(s(x29)), x30))∧(∀x37,x38,x39,x40:plus(x35, x36)=s(x37)∧gt(x38, x37)=true∧(∀x39,x40:gt(x38, x37)=true∧plus(x39, x40)=x37 ⇒ F(true, x38, s(x39), x40)≥F(gt(x38, plus(s(x39), x40)), x38, s(s(x39)), x40)) ⇒ F(true, s(x38), s(x35), x36)≥F(gt(s(x38), plus(s(x35), x36)), s(x38), s(s(x35)), x36)) ⇒ F(true, s(x27), s(x35), s(x36))≥F(gt(s(x27), plus(s(x35), s(x36))), s(x27), s(s(x35)), s(x36)))

We simplified constraint (5) using rule (V) (with possible (I) afterwards) using induction on plus(x1, x2)=0 which results in the following new constraint:
(8)    (x31=0 ⇒ F(true, s(x26), s(x31), 0)≥F(gt(s(x26), plus(s(x31), 0)), s(x26), s(s(x31)), 0))

We simplified constraint (8) using rule (III) which results in the following new constraint:
(9)    (F(true, s(x26), s(0), 0)≥F(gt(s(x26), plus(s(0), 0)), s(x26), s(s(0)), 0))

We simplified constraint (6) using rules (III), (IV) which results in the following new constraint:
(10)    (gt(x27, x28)=true ⇒ F(true, s(x27), s(s(x28)), 0)≥F(gt(s(x27), plus(s(s(x28)), 0)), s(x27), s(s(s(x28))), 0))

We simplified constraint (7) using rules (I), (II) which results in the following new constraint:
(11)    (plus(x35, x36)=x28∧gt(x27, x28)=true∧(∀x29,x30:gt(x27, x28)=true∧plus(x29, x30)=x28 ⇒ F(true, x27, s(x29), x30)≥F(gt(x27, plus(s(x29), x30)), x27, s(s(x29)), x30))∧(∀x37,x38,x39,x40:plus(x35, x36)=s(x37)∧gt(x38, x37)=true∧(∀x39,x40:gt(x38, x37)=true∧plus(x39, x40)=x37 ⇒ F(true, x38, s(x39), x40)≥F(gt(x38, plus(s(x39), x40)), x38, s(s(x39)), x40)) ⇒ F(true, s(x38), s(x35), x36)≥F(gt(s(x38), plus(s(x35), x36)), s(x38), s(s(x35)), x36)) ⇒ F(true, s(x27), s(x35), s(x36))≥F(gt(s(x27), plus(s(x35), s(x36))), s(x27), s(s(x35)), s(x36)))

We simplified constraint (10) using rule (V) (with possible (I) afterwards) using induction on gt(x27, x28)=true which results in the following new constraints:
(12)    (true=true ⇒ F(true, s(s(x42)), s(s(0)), 0)≥F(gt(s(s(x42)), plus(s(s(0)), 0)), s(s(x42)), s(s(s(0))), 0))

(13)    (gt(x43, x44)=true∧(gt(x43, x44)=true ⇒ F(true, s(x43), s(s(x44)), 0)≥F(gt(s(x43), plus(s(s(x44)), 0)), s(x43), s(s(s(x44))), 0)) ⇒ F(true, s(s(x43)), s(s(s(x44))), 0)≥F(gt(s(s(x43)), plus(s(s(s(x44))), 0)), s(s(x43)), s(s(s(s(x44)))), 0))

We simplified constraint (12) using rules (I), (II) which results in the following new constraint:
(14)    (F(true, s(s(x42)), s(s(0)), 0)≥F(gt(s(s(x42)), plus(s(s(0)), 0)), s(s(x42)), s(s(s(0))), 0))

We simplified constraint (13) using rule (VI) where we applied the induction hypothesis (gt(x43, x44)=true ⇒ F(true, s(x43), s(s(x44)), 0)≥F(gt(s(x43), plus(s(s(x44)), 0)), s(x43), s(s(s(x44))), 0)) with σ = [ ] which results in the following new constraint:
(15)    (F(true, s(x43), s(s(x44)), 0)≥F(gt(s(x43), plus(s(s(x44)), 0)), s(x43), s(s(s(x44))), 0) ⇒ F(true, s(s(x43)), s(s(s(x44))), 0)≥F(gt(s(s(x43)), plus(s(s(s(x44))), 0)), s(s(x43)), s(s(s(s(x44)))), 0))

We simplified constraint (11) using rule (VI) where we applied the induction hypothesis (∀x29,x30:gt(x27, x28)=true∧plus(x29, x30)=x28 ⇒ F(true, x27, s(x29), x30)≥F(gt(x27, plus(s(x29), x30)), x27, s(s(x29)), x30)) with σ = [x29 / x35, x30 / x36] which results in the following new constraint:
(16)    (F(true, x27, s(x35), x36)≥F(gt(x27, plus(s(x35), x36)), x27, s(s(x35)), x36)∧(∀x37,x38,x39,x40:plus(x35, x36)=s(x37)∧gt(x38, x37)=true∧(∀x39,x40:gt(x38, x37)=true∧plus(x39, x40)=x37 ⇒ F(true, x38, s(x39), x40)≥F(gt(x38, plus(s(x39), x40)), x38, s(s(x39)), x40)) ⇒ F(true, s(x38), s(x35), x36)≥F(gt(s(x38), plus(s(x35), x36)), s(x38), s(s(x35)), x36)) ⇒ F(true, s(x27), s(x35), s(x36))≥F(gt(s(x27), plus(s(x35), s(x36))), s(x27), s(s(x35)), s(x36)))

We simplified constraint (16) using rule (IV) which results in the following new constraint:
(17)    (F(true, x27, s(x35), x36)≥F(gt(x27, plus(s(x35), x36)), x27, s(s(x35)), x36) ⇒ F(true, s(x27), s(x35), s(x36))≥F(gt(s(x27), plus(s(x35), s(x36))), s(x27), s(s(x35)), s(x36)))
We consider the chain F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z)), F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z) which results in the following constraint:
(18)    (F(gt(x6, plus(x7, x8)), x6, x7, s(x8))=F(true, x9, x10, x11) ⇒ F(true, x9, x10, x11)≥F(gt(x9, plus(x10, x11)), x9, s(x10), x11))

We simplified constraint (18) using rules (I), (II), (III), (VII) which results in the following new constraint:
(19)    (plus(x7, x8)=x45∧gt(x6, x45)=true ⇒ F(true, x6, x7, s(x8))≥F(gt(x6, plus(x7, s(x8))), x6, s(x7), s(x8)))

We simplified constraint (19) using rule (V) (with possible (I) afterwards) using induction on gt(x6, x45)=true which results in the following new constraints:
(20)    (true=true∧plus(x7, x8)=0 ⇒ F(true, s(x47), x7, s(x8))≥F(gt(s(x47), plus(x7, s(x8))), s(x47), s(x7), s(x8)))

(21)    (gt(x48, x49)=true∧plus(x7, x8)=s(x49)∧(∀x50,x51:gt(x48, x49)=true∧plus(x50, x51)=x49 ⇒ F(true, x48, x50, s(x51))≥F(gt(x48, plus(x50, s(x51))), x48, s(x50), s(x51))) ⇒ F(true, s(x48), x7, s(x8))≥F(gt(s(x48), plus(x7, s(x8))), s(x48), s(x7), s(x8)))

We simplified constraint (20) using rules (I), (II) which results in the following new constraint:
(22)    (plus(x7, x8)=0 ⇒ F(true, s(x47), x7, s(x8))≥F(gt(s(x47), plus(x7, s(x8))), s(x47), s(x7), s(x8)))

We simplified constraint (21) using rule (V) (with possible (I) afterwards) using induction on plus(x7, x8)=s(x49) which results in the following new constraints:
(23)    (x55=s(x49)∧gt(x48, x49)=true∧(∀x50,x51:gt(x48, x49)=true∧plus(x50, x51)=x49 ⇒ F(true, x48, x50, s(x51))≥F(gt(x48, plus(x50, s(x51))), x48, s(x50), s(x51))) ⇒ F(true, s(x48), x55, s(0))≥F(gt(s(x48), plus(x55, s(0))), s(x48), s(x55), s(0)))

(24)    (s(plus(x56, x57))=s(x49)∧gt(x48, x49)=true∧(∀x50,x51:gt(x48, x49)=true∧plus(x50, x51)=x49 ⇒ F(true, x48, x50, s(x51))≥F(gt(x48, plus(x50, s(x51))), x48, s(x50), s(x51)))∧(∀x58,x59,x60,x61:plus(x56, x57)=s(x58)∧gt(x59, x58)=true∧(∀x60,x61:gt(x59, x58)=true∧plus(x60, x61)=x58 ⇒ F(true, x59, x60, s(x61))≥F(gt(x59, plus(x60, s(x61))), x59, s(x60), s(x61))) ⇒ F(true, s(x59), x56, s(x57))≥F(gt(s(x59), plus(x56, s(x57))), s(x59), s(x56), s(x57))) ⇒ F(true, s(x48), x56, s(s(x57)))≥F(gt(s(x48), plus(x56, s(s(x57)))), s(x48), s(x56), s(s(x57))))

We simplified constraint (22) using rule (V) (with possible (I) afterwards) using induction on plus(x7, x8)=0 which results in the following new constraint:
(25)    (x52=0 ⇒ F(true, s(x47), x52, s(0))≥F(gt(s(x47), plus(x52, s(0))), s(x47), s(x52), s(0)))

We simplified constraint (25) using rule (III) which results in the following new constraint:
(26)    (F(true, s(x47), 0, s(0))≥F(gt(s(x47), plus(0, s(0))), s(x47), s(0), s(0)))

We simplified constraint (23) using rules (III), (IV) which results in the following new constraint:
(27)    (gt(x48, x49)=true ⇒ F(true, s(x48), s(x49), s(0))≥F(gt(s(x48), plus(s(x49), s(0))), s(x48), s(s(x49)), s(0)))

We simplified constraint (24) using rules (I), (II) which results in the following new constraint:
(28)    (plus(x56, x57)=x49∧gt(x48, x49)=true∧(∀x50,x51:gt(x48, x49)=true∧plus(x50, x51)=x49 ⇒ F(true, x48, x50, s(x51))≥F(gt(x48, plus(x50, s(x51))), x48, s(x50), s(x51)))∧(∀x58,x59,x60,x61:plus(x56, x57)=s(x58)∧gt(x59, x58)=true∧(∀x60,x61:gt(x59, x58)=true∧plus(x60, x61)=x58 ⇒ F(true, x59, x60, s(x61))≥F(gt(x59, plus(x60, s(x61))), x59, s(x60), s(x61))) ⇒ F(true, s(x59), x56, s(x57))≥F(gt(s(x59), plus(x56, s(x57))), s(x59), s(x56), s(x57))) ⇒ F(true, s(x48), x56, s(s(x57)))≥F(gt(s(x48), plus(x56, s(s(x57)))), s(x48), s(x56), s(s(x57))))

We simplified constraint (27) using rule (V) (with possible (I) afterwards) using induction on gt(x48, x49)=true which results in the following new constraints:
(29)    (true=true ⇒ F(true, s(s(x63)), s(0), s(0))≥F(gt(s(s(x63)), plus(s(0), s(0))), s(s(x63)), s(s(0)), s(0)))

(30)    (gt(x64, x65)=true∧(gt(x64, x65)=true ⇒ F(true, s(x64), s(x65), s(0))≥F(gt(s(x64), plus(s(x65), s(0))), s(x64), s(s(x65)), s(0))) ⇒ F(true, s(s(x64)), s(s(x65)), s(0))≥F(gt(s(s(x64)), plus(s(s(x65)), s(0))), s(s(x64)), s(s(s(x65))), s(0)))

We simplified constraint (29) using rules (I), (II) which results in the following new constraint:
(31)    (F(true, s(s(x63)), s(0), s(0))≥F(gt(s(s(x63)), plus(s(0), s(0))), s(s(x63)), s(s(0)), s(0)))

We simplified constraint (30) using rule (VI) where we applied the induction hypothesis (gt(x64, x65)=true ⇒ F(true, s(x64), s(x65), s(0))≥F(gt(s(x64), plus(s(x65), s(0))), s(x64), s(s(x65)), s(0))) with σ = [ ] which results in the following new constraint:
(32)    (F(true, s(x64), s(x65), s(0))≥F(gt(s(x64), plus(s(x65), s(0))), s(x64), s(s(x65)), s(0)) ⇒ F(true, s(s(x64)), s(s(x65)), s(0))≥F(gt(s(s(x64)), plus(s(s(x65)), s(0))), s(s(x64)), s(s(s(x65))), s(0)))

We simplified constraint (28) using rule (VI) where we applied the induction hypothesis (∀x50,x51:gt(x48, x49)=true∧plus(x50, x51)=x49 ⇒ F(true, x48, x50, s(x51))≥F(gt(x48, plus(x50, s(x51))), x48, s(x50), s(x51))) with σ = [x51 / x57, x50 / x56] which results in the following new constraint:
(33)    (F(true, x48, x56, s(x57))≥F(gt(x48, plus(x56, s(x57))), x48, s(x56), s(x57))∧(∀x58,x59,x60,x61:plus(x56, x57)=s(x58)∧gt(x59, x58)=true∧(∀x60,x61:gt(x59, x58)=true∧plus(x60, x61)=x58 ⇒ F(true, x59, x60, s(x61))≥F(gt(x59, plus(x60, s(x61))), x59, s(x60), s(x61))) ⇒ F(true, s(x59), x56, s(x57))≥F(gt(s(x59), plus(x56, s(x57))), s(x59), s(x56), s(x57))) ⇒ F(true, s(x48), x56, s(s(x57)))≥F(gt(s(x48), plus(x56, s(s(x57)))), s(x48), s(x56), s(s(x57))))

We simplified constraint (33) using rule (IV) which results in the following new constraint:
(34)    (F(true, x48, x56, s(x57))≥F(gt(x48, plus(x56, s(x57))), x48, s(x56), s(x57)) ⇒ F(true, s(x48), x56, s(s(x57)))≥F(gt(s(x48), plus(x56, s(s(x57)))), s(x48), s(x56), s(s(x57))))

For Pair F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z)) the following chains were created:

We consider the chain F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z), F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z)) which results in the following constraint:
(35)    (F(gt(x12, plus(x13, x14)), x12, s(x13), x14)=F(true, x15, x16, x17) ⇒ F(true, x15, x16, x17)≥F(gt(x15, plus(x16, x17)), x15, x16, s(x17)))

We simplified constraint (35) using rules (I), (II), (III), (VII) which results in the following new constraint:
(36)    (plus(x13, x14)=x66∧gt(x12, x66)=true ⇒ F(true, x12, s(x13), x14)≥F(gt(x12, plus(s(x13), x14)), x12, s(x13), s(x14)))

We simplified constraint (36) using rule (V) (with possible (I) afterwards) using induction on gt(x12, x66)=true which results in the following new constraints:
(37)    (true=true∧plus(x13, x14)=0 ⇒ F(true, s(x68), s(x13), x14)≥F(gt(s(x68), plus(s(x13), x14)), s(x68), s(x13), s(x14)))

(38)    (gt(x69, x70)=true∧plus(x13, x14)=s(x70)∧(∀x71,x72:gt(x69, x70)=true∧plus(x71, x72)=x70 ⇒ F(true, x69, s(x71), x72)≥F(gt(x69, plus(s(x71), x72)), x69, s(x71), s(x72))) ⇒ F(true, s(x69), s(x13), x14)≥F(gt(s(x69), plus(s(x13), x14)), s(x69), s(x13), s(x14)))

We simplified constraint (37) using rules (I), (II) which results in the following new constraint:
(39)    (plus(x13, x14)=0 ⇒ F(true, s(x68), s(x13), x14)≥F(gt(s(x68), plus(s(x13), x14)), s(x68), s(x13), s(x14)))

We simplified constraint (38) using rule (V) (with possible (I) afterwards) using induction on plus(x13, x14)=s(x70) which results in the following new constraints:
(40)    (x76=s(x70)∧gt(x69, x70)=true∧(∀x71,x72:gt(x69, x70)=true∧plus(x71, x72)=x70 ⇒ F(true, x69, s(x71), x72)≥F(gt(x69, plus(s(x71), x72)), x69, s(x71), s(x72))) ⇒ F(true, s(x69), s(x76), 0)≥F(gt(s(x69), plus(s(x76), 0)), s(x69), s(x76), s(0)))

(41)    (s(plus(x77, x78))=s(x70)∧gt(x69, x70)=true∧(∀x71,x72:gt(x69, x70)=true∧plus(x71, x72)=x70 ⇒ F(true, x69, s(x71), x72)≥F(gt(x69, plus(s(x71), x72)), x69, s(x71), s(x72)))∧(∀x79,x80,x81,x82:plus(x77, x78)=s(x79)∧gt(x80, x79)=true∧(∀x81,x82:gt(x80, x79)=true∧plus(x81, x82)=x79 ⇒ F(true, x80, s(x81), x82)≥F(gt(x80, plus(s(x81), x82)), x80, s(x81), s(x82))) ⇒ F(true, s(x80), s(x77), x78)≥F(gt(s(x80), plus(s(x77), x78)), s(x80), s(x77), s(x78))) ⇒ F(true, s(x69), s(x77), s(x78))≥F(gt(s(x69), plus(s(x77), s(x78))), s(x69), s(x77), s(s(x78))))

We simplified constraint (39) using rule (V) (with possible (I) afterwards) using induction on plus(x13, x14)=0 which results in the following new constraint:
(42)    (x73=0 ⇒ F(true, s(x68), s(x73), 0)≥F(gt(s(x68), plus(s(x73), 0)), s(x68), s(x73), s(0)))

We simplified constraint (42) using rule (III) which results in the following new constraint:
(43)    (F(true, s(x68), s(0), 0)≥F(gt(s(x68), plus(s(0), 0)), s(x68), s(0), s(0)))

We simplified constraint (40) using rules (III), (IV) which results in the following new constraint:
(44)    (gt(x69, x70)=true ⇒ F(true, s(x69), s(s(x70)), 0)≥F(gt(s(x69), plus(s(s(x70)), 0)), s(x69), s(s(x70)), s(0)))

We simplified constraint (41) using rules (I), (II) which results in the following new constraint:
(45)    (plus(x77, x78)=x70∧gt(x69, x70)=true∧(∀x71,x72:gt(x69, x70)=true∧plus(x71, x72)=x70 ⇒ F(true, x69, s(x71), x72)≥F(gt(x69, plus(s(x71), x72)), x69, s(x71), s(x72)))∧(∀x79,x80,x81,x82:plus(x77, x78)=s(x79)∧gt(x80, x79)=true∧(∀x81,x82:gt(x80, x79)=true∧plus(x81, x82)=x79 ⇒ F(true, x80, s(x81), x82)≥F(gt(x80, plus(s(x81), x82)), x80, s(x81), s(x82))) ⇒ F(true, s(x80), s(x77), x78)≥F(gt(s(x80), plus(s(x77), x78)), s(x80), s(x77), s(x78))) ⇒ F(true, s(x69), s(x77), s(x78))≥F(gt(s(x69), plus(s(x77), s(x78))), s(x69), s(x77), s(s(x78))))

We simplified constraint (44) using rule (V) (with possible (I) afterwards) using induction on gt(x69, x70)=true which results in the following new constraints:
(46)    (true=true ⇒ F(true, s(s(x84)), s(s(0)), 0)≥F(gt(s(s(x84)), plus(s(s(0)), 0)), s(s(x84)), s(s(0)), s(0)))

(47)    (gt(x85, x86)=true∧(gt(x85, x86)=true ⇒ F(true, s(x85), s(s(x86)), 0)≥F(gt(s(x85), plus(s(s(x86)), 0)), s(x85), s(s(x86)), s(0))) ⇒ F(true, s(s(x85)), s(s(s(x86))), 0)≥F(gt(s(s(x85)), plus(s(s(s(x86))), 0)), s(s(x85)), s(s(s(x86))), s(0)))

We simplified constraint (46) using rules (I), (II) which results in the following new constraint:
(48)    (F(true, s(s(x84)), s(s(0)), 0)≥F(gt(s(s(x84)), plus(s(s(0)), 0)), s(s(x84)), s(s(0)), s(0)))

We simplified constraint (47) using rule (VI) where we applied the induction hypothesis (gt(x85, x86)=true ⇒ F(true, s(x85), s(s(x86)), 0)≥F(gt(s(x85), plus(s(s(x86)), 0)), s(x85), s(s(x86)), s(0))) with σ = [ ] which results in the following new constraint:
(49)    (F(true, s(x85), s(s(x86)), 0)≥F(gt(s(x85), plus(s(s(x86)), 0)), s(x85), s(s(x86)), s(0)) ⇒ F(true, s(s(x85)), s(s(s(x86))), 0)≥F(gt(s(s(x85)), plus(s(s(s(x86))), 0)), s(s(x85)), s(s(s(x86))), s(0)))

We simplified constraint (45) using rule (VI) where we applied the induction hypothesis (∀x71,x72:gt(x69, x70)=true∧plus(x71, x72)=x70 ⇒ F(true, x69, s(x71), x72)≥F(gt(x69, plus(s(x71), x72)), x69, s(x71), s(x72))) with σ = [x71 / x77, x72 / x78] which results in the following new constraint:
(50)    (F(true, x69, s(x77), x78)≥F(gt(x69, plus(s(x77), x78)), x69, s(x77), s(x78))∧(∀x79,x80,x81,x82:plus(x77, x78)=s(x79)∧gt(x80, x79)=true∧(∀x81,x82:gt(x80, x79)=true∧plus(x81, x82)=x79 ⇒ F(true, x80, s(x81), x82)≥F(gt(x80, plus(s(x81), x82)), x80, s(x81), s(x82))) ⇒ F(true, s(x80), s(x77), x78)≥F(gt(s(x80), plus(s(x77), x78)), s(x80), s(x77), s(x78))) ⇒ F(true, s(x69), s(x77), s(x78))≥F(gt(s(x69), plus(s(x77), s(x78))), s(x69), s(x77), s(s(x78))))

We simplified constraint (50) using rule (IV) which results in the following new constraint:
(51)    (F(true, x69, s(x77), x78)≥F(gt(x69, plus(s(x77), x78)), x69, s(x77), s(x78)) ⇒ F(true, s(x69), s(x77), s(x78))≥F(gt(s(x69), plus(s(x77), s(x78))), s(x69), s(x77), s(s(x78))))
We consider the chain F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z)), F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z)) which results in the following constraint:
(52)    (F(gt(x18, plus(x19, x20)), x18, x19, s(x20))=F(true, x21, x22, x23) ⇒ F(true, x21, x22, x23)≥F(gt(x21, plus(x22, x23)), x21, x22, s(x23)))

We simplified constraint (52) using rules (I), (II), (III), (VII) which results in the following new constraint:
(53)    (plus(x19, x20)=x87∧gt(x18, x87)=true ⇒ F(true, x18, x19, s(x20))≥F(gt(x18, plus(x19, s(x20))), x18, x19, s(s(x20))))

We simplified constraint (53) using rule (V) (with possible (I) afterwards) using induction on gt(x18, x87)=true which results in the following new constraints:
(54)    (true=true∧plus(x19, x20)=0 ⇒ F(true, s(x89), x19, s(x20))≥F(gt(s(x89), plus(x19, s(x20))), s(x89), x19, s(s(x20))))

(55)    (gt(x90, x91)=true∧plus(x19, x20)=s(x91)∧(∀x92,x93:gt(x90, x91)=true∧plus(x92, x93)=x91 ⇒ F(true, x90, x92, s(x93))≥F(gt(x90, plus(x92, s(x93))), x90, x92, s(s(x93)))) ⇒ F(true, s(x90), x19, s(x20))≥F(gt(s(x90), plus(x19, s(x20))), s(x90), x19, s(s(x20))))

We simplified constraint (54) using rules (I), (II) which results in the following new constraint:
(56)    (plus(x19, x20)=0 ⇒ F(true, s(x89), x19, s(x20))≥F(gt(s(x89), plus(x19, s(x20))), s(x89), x19, s(s(x20))))

We simplified constraint (55) using rule (V) (with possible (I) afterwards) using induction on plus(x19, x20)=s(x91) which results in the following new constraints:
(57)    (x97=s(x91)∧gt(x90, x91)=true∧(∀x92,x93:gt(x90, x91)=true∧plus(x92, x93)=x91 ⇒ F(true, x90, x92, s(x93))≥F(gt(x90, plus(x92, s(x93))), x90, x92, s(s(x93)))) ⇒ F(true, s(x90), x97, s(0))≥F(gt(s(x90), plus(x97, s(0))), s(x90), x97, s(s(0))))

(58)    (s(plus(x98, x99))=s(x91)∧gt(x90, x91)=true∧(∀x92,x93:gt(x90, x91)=true∧plus(x92, x93)=x91 ⇒ F(true, x90, x92, s(x93))≥F(gt(x90, plus(x92, s(x93))), x90, x92, s(s(x93))))∧(∀x100,x101,x102,x103:plus(x98, x99)=s(x100)∧gt(x101, x100)=true∧(∀x102,x103:gt(x101, x100)=true∧plus(x102, x103)=x100 ⇒ F(true, x101, x102, s(x103))≥F(gt(x101, plus(x102, s(x103))), x101, x102, s(s(x103)))) ⇒ F(true, s(x101), x98, s(x99))≥F(gt(s(x101), plus(x98, s(x99))), s(x101), x98, s(s(x99)))) ⇒ F(true, s(x90), x98, s(s(x99)))≥F(gt(s(x90), plus(x98, s(s(x99)))), s(x90), x98, s(s(s(x99)))))

We simplified constraint (56) using rule (V) (with possible (I) afterwards) using induction on plus(x19, x20)=0 which results in the following new constraint:
(59)    (x94=0 ⇒ F(true, s(x89), x94, s(0))≥F(gt(s(x89), plus(x94, s(0))), s(x89), x94, s(s(0))))

We simplified constraint (59) using rule (III) which results in the following new constraint:
(60)    (F(true, s(x89), 0, s(0))≥F(gt(s(x89), plus(0, s(0))), s(x89), 0, s(s(0))))

We simplified constraint (57) using rules (III), (IV) which results in the following new constraint:
(61)    (gt(x90, x91)=true ⇒ F(true, s(x90), s(x91), s(0))≥F(gt(s(x90), plus(s(x91), s(0))), s(x90), s(x91), s(s(0))))

We simplified constraint (58) using rules (I), (II) which results in the following new constraint:
(62)    (plus(x98, x99)=x91∧gt(x90, x91)=true∧(∀x92,x93:gt(x90, x91)=true∧plus(x92, x93)=x91 ⇒ F(true, x90, x92, s(x93))≥F(gt(x90, plus(x92, s(x93))), x90, x92, s(s(x93))))∧(∀x100,x101,x102,x103:plus(x98, x99)=s(x100)∧gt(x101, x100)=true∧(∀x102,x103:gt(x101, x100)=true∧plus(x102, x103)=x100 ⇒ F(true, x101, x102, s(x103))≥F(gt(x101, plus(x102, s(x103))), x101, x102, s(s(x103)))) ⇒ F(true, s(x101), x98, s(x99))≥F(gt(s(x101), plus(x98, s(x99))), s(x101), x98, s(s(x99)))) ⇒ F(true, s(x90), x98, s(s(x99)))≥F(gt(s(x90), plus(x98, s(s(x99)))), s(x90), x98, s(s(s(x99)))))

We simplified constraint (61) using rule (V) (with possible (I) afterwards) using induction on gt(x90, x91)=true which results in the following new constraints:
(63)    (true=true ⇒ F(true, s(s(x105)), s(0), s(0))≥F(gt(s(s(x105)), plus(s(0), s(0))), s(s(x105)), s(0), s(s(0))))

(64)    (gt(x106, x107)=true∧(gt(x106, x107)=true ⇒ F(true, s(x106), s(x107), s(0))≥F(gt(s(x106), plus(s(x107), s(0))), s(x106), s(x107), s(s(0)))) ⇒ F(true, s(s(x106)), s(s(x107)), s(0))≥F(gt(s(s(x106)), plus(s(s(x107)), s(0))), s(s(x106)), s(s(x107)), s(s(0))))

We simplified constraint (63) using rules (I), (II) which results in the following new constraint:
(65)    (F(true, s(s(x105)), s(0), s(0))≥F(gt(s(s(x105)), plus(s(0), s(0))), s(s(x105)), s(0), s(s(0))))

We simplified constraint (64) using rule (VI) where we applied the induction hypothesis (gt(x106, x107)=true ⇒ F(true, s(x106), s(x107), s(0))≥F(gt(s(x106), plus(s(x107), s(0))), s(x106), s(x107), s(s(0)))) with σ = [ ] which results in the following new constraint:
(66)    (F(true, s(x106), s(x107), s(0))≥F(gt(s(x106), plus(s(x107), s(0))), s(x106), s(x107), s(s(0))) ⇒ F(true, s(s(x106)), s(s(x107)), s(0))≥F(gt(s(s(x106)), plus(s(s(x107)), s(0))), s(s(x106)), s(s(x107)), s(s(0))))

We simplified constraint (62) using rule (VI) where we applied the induction hypothesis (∀x92,x93:gt(x90, x91)=true∧plus(x92, x93)=x91 ⇒ F(true, x90, x92, s(x93))≥F(gt(x90, plus(x92, s(x93))), x90, x92, s(s(x93)))) with σ = [x92 / x98, x93 / x99] which results in the following new constraint:
(67)    (F(true, x90, x98, s(x99))≥F(gt(x90, plus(x98, s(x99))), x90, x98, s(s(x99)))∧(∀x100,x101,x102,x103:plus(x98, x99)=s(x100)∧gt(x101, x100)=true∧(∀x102,x103:gt(x101, x100)=true∧plus(x102, x103)=x100 ⇒ F(true, x101, x102, s(x103))≥F(gt(x101, plus(x102, s(x103))), x101, x102, s(s(x103)))) ⇒ F(true, s(x101), x98, s(x99))≥F(gt(s(x101), plus(x98, s(x99))), s(x101), x98, s(s(x99)))) ⇒ F(true, s(x90), x98, s(s(x99)))≥F(gt(s(x90), plus(x98, s(s(x99)))), s(x90), x98, s(s(s(x99)))))

We simplified constraint (67) using rule (IV) which results in the following new constraint:
(68)    (F(true, x90, x98, s(x99))≥F(gt(x90, plus(x98, s(x99))), x90, x98, s(s(x99))) ⇒ F(true, s(x90), x98, s(s(x99)))≥F(gt(s(x90), plus(x98, s(s(x99)))), s(x90), x98, s(s(s(x99)))))

To summarize, we get the following constraints P_≥ for the following pairs.

F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z)
- (F(true, s(x26), s(0), 0)≥F(gt(s(x26), plus(s(0), 0)), s(x26), s(s(0)), 0))
- (F(true, s(s(x42)), s(s(0)), 0)≥F(gt(s(s(x42)), plus(s(s(0)), 0)), s(s(x42)), s(s(s(0))), 0))
- (F(true, s(x43), s(s(x44)), 0)≥F(gt(s(x43), plus(s(s(x44)), 0)), s(x43), s(s(s(x44))), 0) ⇒ F(true, s(s(x43)), s(s(s(x44))), 0)≥F(gt(s(s(x43)), plus(s(s(s(x44))), 0)), s(s(x43)), s(s(s(s(x44)))), 0))
- (F(true, x27, s(x35), x36)≥F(gt(x27, plus(s(x35), x36)), x27, s(s(x35)), x36) ⇒ F(true, s(x27), s(x35), s(x36))≥F(gt(s(x27), plus(s(x35), s(x36))), s(x27), s(s(x35)), s(x36)))
- (F(true, s(x47), 0, s(0))≥F(gt(s(x47), plus(0, s(0))), s(x47), s(0), s(0)))
- (F(true, s(s(x63)), s(0), s(0))≥F(gt(s(s(x63)), plus(s(0), s(0))), s(s(x63)), s(s(0)), s(0)))
- (F(true, s(x64), s(x65), s(0))≥F(gt(s(x64), plus(s(x65), s(0))), s(x64), s(s(x65)), s(0)) ⇒ F(true, s(s(x64)), s(s(x65)), s(0))≥F(gt(s(s(x64)), plus(s(s(x65)), s(0))), s(s(x64)), s(s(s(x65))), s(0)))
- (F(true, x48, x56, s(x57))≥F(gt(x48, plus(x56, s(x57))), x48, s(x56), s(x57)) ⇒ F(true, s(x48), x56, s(s(x57)))≥F(gt(s(x48), plus(x56, s(s(x57)))), s(x48), s(x56), s(s(x57))))
F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z))
- (F(true, s(x68), s(0), 0)≥F(gt(s(x68), plus(s(0), 0)), s(x68), s(0), s(0)))
- (F(true, s(s(x84)), s(s(0)), 0)≥F(gt(s(s(x84)), plus(s(s(0)), 0)), s(s(x84)), s(s(0)), s(0)))
- (F(true, s(x85), s(s(x86)), 0)≥F(gt(s(x85), plus(s(s(x86)), 0)), s(x85), s(s(x86)), s(0)) ⇒ F(true, s(s(x85)), s(s(s(x86))), 0)≥F(gt(s(s(x85)), plus(s(s(s(x86))), 0)), s(s(x85)), s(s(s(x86))), s(0)))
- (F(true, x69, s(x77), x78)≥F(gt(x69, plus(s(x77), x78)), x69, s(x77), s(x78)) ⇒ F(true, s(x69), s(x77), s(x78))≥F(gt(s(x69), plus(s(x77), s(x78))), s(x69), s(x77), s(s(x78))))
- (F(true, s(x89), 0, s(0))≥F(gt(s(x89), plus(0, s(0))), s(x89), 0, s(s(0))))
- (F(true, s(s(x105)), s(0), s(0))≥F(gt(s(s(x105)), plus(s(0), s(0))), s(s(x105)), s(0), s(s(0))))
- (F(true, s(x106), s(x107), s(0))≥F(gt(s(x106), plus(s(x107), s(0))), s(x106), s(x107), s(s(0))) ⇒ F(true, s(s(x106)), s(s(x107)), s(0))≥F(gt(s(s(x106)), plus(s(s(x107)), s(0))), s(s(x106)), s(s(x107)), s(s(0))))
- (F(true, x90, x98, s(x99))≥F(gt(x90, plus(x98, s(x99))), x90, x98, s(s(x99))) ⇒ F(true, s(x90), x98, s(s(x99)))≥F(gt(s(x90), plus(x98, s(s(x99)))), s(x90), x98, s(s(s(x99)))))

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [18]:

POL(0) = 0
POL(F(x₁, x₂, x₃, x₄)) = -1 - x₁ + x₂ - x₃ - x₄
POL(c) = -2
POL(false) = 1
POL(gt(x₁, x₂)) = 1
POL(plus(x₁, x₂)) = 0
POL(s(x₁)) = 1 + x₁
POL(true) = 1

The following pairs are in P_>:

F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z)
F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z))

The following pairs are in P_bound:

F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z)
F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z))

The following rules are usable:

false → gt(0, v)
gt(u, v) → gt(s(u), s(v))
true → gt(s(u), 0)

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ NonInfProof

                          ↳ QDP

                            ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

plus(x0, 0)
plus(x0, s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.